Verification¶
Commands¶
Imandra has a number of powerful verification commands:
verify <func>: takes a function representing a goal and attempts to prove it. If the proof attempt fails, Imandra will try to synthesize a concrete counterexample illustrating the failure. Found counterexamples are installed by Imandra in theCXmodule. When verifying a formula that doesn't depend on function parameters,verify (<expr>)is a shorthand forverify (fun () -> <expr>)instance <func>: takes a function representing a goal and attempts to synthesize an instance (i.e., a concrete value) that satisfies it. It is useful for answering the question "What is an example value that satisfies this particular property?". Found instances are installed by Imandra in theCXmodule.theorem <name> <vars> = <body>: takes a name, variables and a function of the variables representing a goal to be proved. If Imandra proves the goal, the named theorem is installed and may be used in subsequent proofs. Theorems can be tagged with attributes instructing Imandra how the theorem should be (automatically) applied to prove other theorems in the future. Found counterexamples are installed by Imandra in theCXmodule.lemma <name> <vars> = <body>: synonym oftheorem, but idiomatically often used for "smaller" subsidiary results as one is working up to a largertheorem.axiom <name> <vars> = <body>: declares an axiom, effectively the same astheorembut forcing Imandra to assume the truth of the conjecture, rather than verifying it. This is of course dangerous and should be used with extreme care.
Examples¶
In [1]:
verify (fun x -> x + 1 > x)
Out[1]:
- : int -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 0 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.040s | ||||||||||||
| details | Expand
|
Expand
start[0.040s] (:var_0: + 1) > :var_0:
simplify
into true
expansions []
rewrite_steps forward_chaining unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
In [2]:
instance (fun x y -> x < 0 && x + y = 4)
Out[2]:
- : int -> Z.t -> bool = <fun> module CX : sig val x : Z.t val y : Z.t end
Instance (after 0 steps, 0.038s): let x = (-1) let y = 5
Instance
Loading..
proof attempt
| ground_instances | 0 | ||||||||||||||||||||
| definitions | 0 | ||||||||||||||||||||
| inductions | 0 | ||||||||||||||||||||
| search_time | 0.038s | ||||||||||||||||||||
| details | Expand
|
Expand
start[0.038s] :var_0: < 0 && :var_0: + :var_1: = 4
simplify
into not (0 <= :var_0:) && :var_0: + :var_1: = 4
expansions []
rewrite_steps forward_chaining - Sat (Some let x = (-1) let y = 5 )
Loading..
In [3]:
theorem succ_mono n m = succ n > succ m <==> n > m
Out[3]:
val succ_mono : int -> int -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 0 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.028s | ||||||||||||
| details | Expand
|
Expand
start[0.028s] (:var_0: + 1) > (:var_1: + 1) = :var_0: > :var_1:
simplify
into true
expansions []
rewrite_steps forward_chaining unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
In [4]:
verify (fun n -> succ n <> 100)
Out[4]:
- : Z.t -> bool = <fun> module CX : sig val n : Z.t end
Counterexample (after 0 steps, 0.028s): let n = 99
Refuted
Loading..
proof attempt
| ground_instances | 0 | ||||||||||||||
| definitions | 0 | ||||||||||||||
| inductions | 0 | ||||||||||||||
| search_time | 0.028s | ||||||||||||||
| details | Expand
|
Expand
start[0.028s] not (:var_0: + 1 = 100)
simplify
into not (:var_0: = 99)
expansions []
rewrite_steps forward_chaining - Sat (Some let n = 99 )
Loading..
Attributes¶
Attributes can be used to give Imandra verification hints, and to instruct Imandra how it should use a proved theorem in subsequent verification efforts, via the installation of a theorem as a "rule".
Verification Hints¶
[@@auto]: apply Imandra's "inductive waterfall" proof strategy, which combines simplification (including automatic subgoaling, conditional rewriting and forward-chaining using previously proved lemmas, decision procedures for datatypes and arithmetic, etc.), and may decide to do induction. This is the most common way to prove atheoremin Imandra.[@@induct <flag?>]: apply Imandra's "inductive waterfall" proof strategy, but control the top-level induction. The<flag?>can be one of:functional <func_name>- perform functional induction using an induction scheme derived from<func_name>structural <args?>- perform structural induction on the arguments<args?>if given, else on a heuristically chosen collection of variables. The types of the induction variables must be algebraic datatypes / variant types. An additive approach (linear in the total number of constructors) is taken for combining the schemes of individual variables into a composite induction scheme.structural_mult <args?>- likestructural, except uses a "multiplicative" scheme, rather than an additive onestructural_add <args?>- a synonym forstructural
[@@simp]or[@@simplify]: apply simplification to the goal before unrolling.[@@disable <f_1>,...,<f_k>]: Iff_iis a rule, instructs Imandra to ignoref_iduring the proof attempt. Iff_iis a function, instructs Imandra to leave the function definition unexpanded during the proof attempt. This is especially useful in the presence of rewrite rules about non-recursive functions, as such rules will typically not apply unless the relevant non-recursive function is disabled. Imandra might choose to ignore this hint if ignoring it leads to immediate closure of the goal, or to the construction of a valid counterexample. Note that rules and functions can be globally disabled, using the#disabledirective.[@@enable <f_1>,...,<f_k>]: The dual of@@disable. Note that rules and functions can be globally enabled, using the#enabledirective.[@@apply <thm <arg_1> ... <arg_k>>]: instantiatethmwith the given arguments and add its instantiation to the hypotheses of the goal. This is especially useful whenthmis not naturally useable as a@@rewriteor@@forward-chainingrule, but is nevertheless needed (in an instantiated form) to prove a given theorem.[@@blast]: apply Imandra's blast procedure, which combines symbolic execution and SAT-based bit-blasting. This is useful for difficult combinatorial problems, and problems involving nontrivial (i.e., nonlinear) arithmetic over bounded discrete domains.
Rule Classes¶
Theorems may be installed as rules, which instructs Imandra to apply them in certain ways during subsequent proof attempts. The development of an appropriate collection of rules can be used to "teach" Imandra how to reason in a new domain.
[@@rw]or[@@rewrite]: install theorem as a rewrite rule[@@fc]or[@@forward-chaining]: install theorem as a forward chaining rule
Examples¶
In [5]:
verify (fun x y -> List.length (x@y) = List.length x + List.length y) [@@auto]
Out[5]:
- : 'a list -> 'a list -> bool = <fun> Goal: List.length (x @ y) = List.length x + List.length y. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length (List.append x y) = List.length x + List.length y Verified up to bound 10 (after 0.183s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from List.append. Induction scheme: (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x). 2 nontautological subgoals. Subgoal 1.2: H0. x = [] |--------------------------------------------------------------------------- List.length (List.append x y) = List.length x + List.length y But simplification reduces this to true, using the definitions of List.append and List.length. Subgoal 1.1: H0. not (x = []) H1. List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y |--------------------------------------------------------------------------- List.length (List.append x y) = List.length x + List.length y But simplification reduces this to true, using the definitions of List.append and List.length.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.339s |
Expand
start[0.339s, "Goal"] List.length (List.append :var_0: :var_1:) = List.length :var_0: + List.length :var_1:
subproof
List.length (List.append x y) = List.length x + List.length ystart[0.339s, "1"] List.length (List.append x y) = List.length x + List.length y
induction on (functional ) :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
Split ((not (x = []) || List.length (List.append x y) = List.length x + List.length y) && (not (not (x = []) && List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y) || List.length (List.append x y) = List.length x + List.length y) :cases [not (x = []) || List.length (List.append x y) = List.length x + List.length y; (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length y])subproof
(x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length ystart[0.049s, "1.1"] (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length ysimplify
into true
expansions [List.length, List.length, List.append]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
subproof
not (x = []) || List.length (List.append x y) = List.length x + List.length ystart[0.049s, "1.2"] not (x = []) || List.length (List.append x y) = List.length x + List.length y
simplify
into true
expansions [List.length, List.append]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
Loading..
In [6]:
verify (fun x -> x @ [] @ x = x @ x) [@@simp]
Out[6]:
- : 'a list -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 1 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.061s | ||||||||||||
| details | Expand
|
Expand
start[0.061s] List.append :var_0: (List.append [] :var_0:) = List.append :var_0: :var_0:
simplify
into true
expansions List.append
rewrite_steps forward_chaining unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
In [7]:
lemma len_append x y = List.length (x@y) = List.length x + List.length y [@@auto] [@@rw]
Out[7]:
val len_append : 'a list -> 'a list -> bool = <fun> Goal: List.length (x @ y) = List.length x + List.length y. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length (List.append x y) = List.length x + List.length y Verified up to bound 10 (after 0.022s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from List.append. Induction scheme: (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x). 2 nontautological subgoals. Subgoal 1.2: H0. x = [] |--------------------------------------------------------------------------- List.length (List.append x y) = List.length x + List.length y But simplification reduces this to true, using the definitions of List.append and List.length. Subgoal 1.1: H0. not (x = []) H1. List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y |--------------------------------------------------------------------------- List.length (List.append x y) = List.length x + List.length y But simplification reduces this to true, using the definitions of List.append and List.length.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.123s |
Expand
start[0.123s, "Goal"] List.length (List.append :var_0: :var_1:) = List.length :var_0: + List.length :var_1:
subproof
List.length (List.append x y) = List.length x + List.length ystart[0.123s, "1"] List.length (List.append x y) = List.length x + List.length y
induction on (functional ) :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
Split ((not (x = []) || List.length (List.append x y) = List.length x + List.length y) && (not (not (x = []) && List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y) || List.length (List.append x y) = List.length x + List.length y) :cases [not (x = []) || List.length (List.append x y) = List.length x + List.length y; (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length y])subproof
(x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length ystart[0.055s, "1.1"] (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length ysimplify
into true
expansions [List.length, List.length, List.append]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
subproof
not (x = []) || List.length (List.append x y) = List.length x + List.length ystart[0.055s, "1.2"] not (x = []) || List.length (List.append x y) = List.length x + List.length y
simplify
into true
expansions [List.length, List.append]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
Loading..
In [8]:
theorem len_non_neg x = (List.length x) [@trigger] >= 0 [@@simp] [@@fc]
Out[8]:
val len_non_neg : 'a list -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 0 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.071s | ||||||||||||
| details | Expand
|
Expand
start[0.071s] List.length :var_0: >= 0
simplify
into true
expansions []
rewrite_steps forward_chaining List.len_nonnegative
unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
In [9]:
lemma foo = (fun x -> x @ [] = x) [@@induct x] [@@disable List.append_to_nil]
Out[9]:
val foo : 'a list -> bool = <fun> Goal: x @ [] = x. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.append x [] = x Verified up to bound 10 (after 0.062s). Must try induction. Induction scheme: φ [] && (x <> [] && φ (List.tl x) ==> φ x). 2 nontautological subgoals. Subgoal 1.2: |--------------------------------------------------------------------------- List.append [] [] = [] But simplification reduces this to true, using the definition of List.append. Subgoal 1.1: H0. x <> [] H1. List.append (List.tl x) [] = List.tl x |--------------------------------------------------------------------------- List.append x [] = x But simplification reduces this to true, using the definition of List.append.
Proved
proof
| ground_instances | 0 |
| definitions | 2 |
| inductions | 1 |
| search_time | 0.157s |
Expand
start[0.157s, "Goal"] List.append :var_0: [] = :var_0:
subproof
List.append x [] = xstart[0.157s, "1"] List.append x [] = x
induction on (structural+ x) :scheme φ [] && (x <> [] && φ (List.tl x) ==> φ x)
Split (List.append [] [] = [] && (not (x <> [] && List.append (List.tl x) [] = List.tl x) || List.append x [] = x) :cases [List.append [] [] = []; (not (x <> []) || not (List.append (List.tl x) [] = List.tl x)) || List.append x [] = x])subproof
(not (x <> []) || not (List.append (List.tl x) [] = List.tl x)) || List.append x [] = xstart[0.070s, "1.1"] (not (x <> []) || not (List.append (List.tl x) [] = List.tl x)) || List.append x [] = x
simplify
into true
expansions List.append
rewrite_steps forward_chaining
subproof
List.append [] [] = []start[0.070s, "1.2"] List.append [] [] = []
simplify
into true
expansions List.append
rewrite_steps forward_chaining
Loading..
Verifying our Programs¶
Now that we've learned the syntax of Imandra's verification statements, let's learn how we can use them to:
verify the absence of bugs,
generate counterexamples and test cases, and
prove program properties.
Unrolling¶
The first tool that Imandra makes available in our verification toolbox is
recursive function unrolling, a form of bounded model checking backed by
Satisfiability Modulo Theories (SMT) solving. This technique is completely
automatic, and is in general not influenced by the presence of proved rules or
enabled/disabled functions (except with used in conjunction with the [@@simp]
attribute).
Completeness¶
For many classes of problems, unrolling is "complete" in various senses. For example, for goals involving only non-recursive functions, algebraic datatypes and linear arithmetic, unrolling will always be able to prove a true goal or refute a false goal in a finite amount of time and space. Moreover, for an even wider class of problems involving recursive functions, datatypes and arithmetic, unrolling is "complete for counterexamples." This means that if a counterexample to a goal exists, unrolling will in principle always be able to synthesize one. This relies on Imandra's "fair" strategy for incrementally expanding the "interpretation call-graph" of a goal.
That said, part of the beauty of unrolling is that you don't need to understand it to apply it!
Strategy¶
In general, it's recommended to apply unrolling to a goal before you attempt
other methods such as the inductive waterfall ([@@auto]). It's amazing how
often seemingly true goals are false due to subtle edge cases, and the ability
of unrolling to construct concrete counterexamples can be an invaluable filter
on your conjectures.
Examples¶
To use unrolling, we simply use the verify or instance commands.
Let's use unrolling to find an instance of two lists of integers, whose sum
equals the length of the two lists concatenated. We shall constrain the total
length of the two lists to be positive (for fun, at least 10), so we obtain
something more interesting than the simple x=[],y=[] solution!
In [10]:
instance
(fun x y -> List.length (x@y) > 10
&& List.fold_left (+) 0 (x@y) = List.length (x@y))
Out[10]:
- : Z.t list -> Z.t list -> bool = <fun> module CX : sig val x : Z.t list val y : Z.t list end
Instance (after 31 steps, 0.233s): let x = [2328] let y = [8855; 3609; 1796; (-1); 0; 4679; (-5828); (-13966); 2455; (-3916)]
Instance
Loading..
proof attempt
| ground_instances | 31 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time | 0.233s | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| details | Expand
|
Expand
start[0.233s] List.length (List.append :var_0: :var_1:) > 10 && List.fold_left + 0 (List.append :var_0: :var_1:) = List.length (List.append :var_0: :var_1:)simplify
into not (List.length (List.append :var_0: :var_1:) <= 10) && List.fold_left + 0 (List.append :var_0: :var_1:) = List.length (List.append :var_0: :var_1:)
expansions []
rewrite_steps forward_chaining - unroll
expr (|`List.fold_left +[0]`_2731| 0 (|List.append_2723| x_2715 y_2716))
expansions - unroll
expr (|List.append_2723| x_2715 y_2716)
expansions - unroll
expr (|List.length_2728| (|List.append_2723| x_2715 y_2716))
expansions - unroll
expr (|`List.fold_left +[0]`_2731| (+ 0 (|get.::.0_2721| (|List.append_2723| x_2715 y_2716))) (|get.:…
expansions - unroll
expr (|List.append_2723| (|get.::.1_2722| x_2715) y_2716)
expansions - unroll
expr (|List.length_2728| (|get.::.1_2722| (|List.append_2723| x_2715 y_2716)))
expansions - unroll
expr (let ((a!1 (+ 0 (|get.::.0_2721| (|List.append_2723| x_2715 y_2716)) (|g…expansions - unroll
expr (|List.length_2728| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| x_2715 y_2716))))
expansions - unroll
expr (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (|List.append_2723| (|get.::.1_2722| (|get.::.1_2722| x_2715)) y_2716)
expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (|List.append_2723| (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| x_2715))) y_2716)
expansions - unroll
expr (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| x_2715)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| x_2715)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| x_2715)))))) (|List…
expansions - unroll
expr (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| …expansions - Sat (Some let x = [2328] let y = [8855; 3609; 1796; (-1); 0; 4679; (-5828); (-13966); 2455; (-3916)] )
Loading..
Imandra was able to find a solution instantly, and reflected it into our runtime
in the CX module. Let's compute with it to better understand it:
In [11]:
List.length (CX.x@CX.y);;
List.fold_left (+) 0 (CX.x@CX.y);;
Out[11]:
- : Z.t = 11 - : Z.t = 11
Unrolling limit¶
Unrolling works by creating a symbolic call graph for the negation of the goal
we've asked Imandra to verify (or dually the positive version of the goal in
the case of instance), and by iteratively extending this graph with
incremental interpretations of recursive functions, up to a given unrolling
bound, checking at each step for satisfiability.
If at any step of the unrolling process the negation of our original goal is
satisfiable w.r.t. the interpreted approximations of the recursive functions,
then Imandra has found a counterexample for our original goal, which has thus
been refuted. In this case, Imandra will report Counterexample (after m steps)
and install the found counterexample in the CX module.
If, on the other hand, Imandra is able to prove that there is no counterexample
in a manner that is independent of the bound on the approximations, then our
original goal is indeed a theorem valid for all possible inputs, and Imandra
will report Theorem Proved. This can always be done for a wide class of
theorems on catamorphisms (e.g.,
List.fold_right), for example.
Otherwise, if Imandra failed to find a counterexample or proof and stopped
unrolling at the unrolling bound, we obtain a weaker result of the form
Unknown (verified up to depth k), which effectively means: this may or may not
be a theorem, but there are no counterexamples up to depth k. Such bounded
results can nevertheless be very useful.
The unrolling bound defaults to 100 and can be controlled using the #unroll <n>
directive.
Let's try to understand in practice how the unrolling bound plays into
unrolling. Consider this simple function that recursively decreases an integer
until it reaches 0, then returns 1:
In [12]:
let rec f x =
if x <= 0 then
1
else
f (x - 1)
Out[12]:
val f : int -> Z.t = <fun>
termination proof
Termination proof
call `f (x - 1)` from `f x`
| original | f x | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | f (x - 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if x >= 0 then x else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (x - 1) >= 0 then x - 1 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (x <= 0)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
Let's verify that for all x < 100, the function will return 1:
In [13]:
verify (fun x -> x < 100 ==> f x = 1)
Out[13]:
- : int -> bool = <fun>
Proved
proof
| ground_instances | 100 | ||||||||||||||||||||||||||||||||
| definitions | 0 | ||||||||||||||||||||||||||||||||
| inductions | 0 | ||||||||||||||||||||||||||||||||
| search_time | 0.973s | ||||||||||||||||||||||||||||||||
| details | Expand
|
Expand
start[0.973s] :var_0: < 100 ==> f :var_0: = 1
simplify
into 100 <= :var_0: || f :var_0: = 1
expansions []
rewrite_steps forward_chaining - unroll
expr (f_2748 x_2761)
expansions - unroll
expr (f_2748 (+ (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions unsat
(let ((a!1 (= (ite (<= x_2761 99) 1 (f_2748 (+ (- 100) x_2761))) 1)) (a!3 (monotonicity (rewri…
Loading..
Loading..
But watch what happens if we ask Imandra to verify this for x < 101,
thus exceding the number of recursive calls that Imandra unrolls by
default:
In [14]:
verify (fun x -> x < 101 ==> f x = 1)
Out[14]:
- : int -> bool = <fun>
Unknown (Verified up to bound 100)
Expand
| expanded |
|
| blocked |
|
Loading..
proof attempt
| ground_instances | 100 |
| definitions | 0 |
| inductions | 0 |
| search_time | 0.238s |
Expand
start[0.238s] :var_0: < 101 ==> f :var_0: = 1
simplify
into 101 <= :var_0: || f :var_0: = 1
expansions []
rewrite_steps forward_chaining - unroll
expr (f_2748 x_2772)
expansions - unroll
expr (f_2748 (+ (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2772))
expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions
Loading..
As expected, since the recursion depth needed to prove this exceeds the
unrolling bound we set, Imandra could only prove this property up to bound
k. This goal is in fact a property that is better suited for verification by
induction (indeed, you might try adding the [@@auto] annotation
to the above goal to invoke the Imandra's inductive waterfall and prove it).
Simplification¶
At the heart of Imandra is a powerful symbolic simplifier and partial
evaluator. The simplifier is
integrated with the inductive waterfall (e.g., [@@auto]), and is the main way
in which previously proved lemmas are used during proofs, through the automatic
application of [@@rewrite] and [@@forward-chaining] rules. The simplifier
can also be used as a pre-processing step before unrolling, via the [@@simp]
attribute.
As the name suggests, simplification is a process that attempts to transform a
formula into a "simpler" form, bringing the salient features of a formula or
conjecture to the surface. Simplification can also prove goals by reducing them
to true, and refute them by reducing them to false.
Notably, because the symbolic evaluation semantics of the simplifier operate on a compact digraph representation of formulas and function definitions, simplification can be thought as having memoized semantics for free.
We can see an example of this by using the following naive recursive version of the fibonacci function:
In [15]:
let rec fib n =
if n <= 1 then
1
else
fib (n-1) + fib (n-2)
Out[15]:
val fib : int -> Z.t = <fun>
termination proof
Termination proof
call `fib (n - 1)` from `fib n`
| original | fib n | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | fib (n - 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if n >= 0 then n else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (n <= 1)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
call `fib (n - 2)` from `fib n`
| original | fib n | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | fib (n - 2) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if n >= 0 then n else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (n - 2) >= 0 then n - 2 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (n <= 1)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
If we try to use Imandra's simplification to search for a solution for fib 200,
Imandra comes back to us with a solution immediately:
In [16]:
#check_models false;;
instance (fun x -> x = fib 200) [@@simp];;
#check_models true;;
Out[16]:
- : Z.t -> bool = <fun> module CX : sig val x : Z.t end
Instance (after 0 steps, 0.054s): let x = 453973694165307953197296969697410619233826
Instance
Loading..
proof attempt
| ground_instances | 0 | ||||||||||||||
| definitions | 201 | ||||||||||||||
| inductions | 0 | ||||||||||||||
| search_time | 0.054s | ||||||||||||||
| details | Expand
|
Expand
start[0.054s] :var_0: = fib 200
simplify
into x = 453973694165307953197296969697410619233826
expansions [fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib]
rewrite_steps forward_chaining - Sat (Some let x = 453973694165307953197296969697410619233826 )
Loading..
If, however, we tried to use normal OCaml evaluation to compute fib 200, OCaml
would take over 10 minutes in order to come back with a response (the
#check_models false command here is used to tell Imandra not to check the
instance Imandra computed using OCaml evaluation, as that requires the expensive
computation of fib 200 via standard OCaml evaluation, which is not memoized).
Now that we know what simplification does, let's learn about how to influence it using rewrite and forward chaining rules.
Rewrite Rules¶
A rewrite rule is a theorem of the form
h_1 && ... && h_k ==> lhs = rhswhich Imandra can use in further proofs to replace terms that match with lhs
(the "left hand side") with the appropriate instantiation of rhs (the "right
hand side"), provided that the instantiations of the hypotheses can be
established. Observe that rewrite rules are both conditional (requiring in
general the establishment of hypotheses) and directed (replacing lhs with
rhs). The lhs is also called the "pattern" of the rule.
An enabled rewrite rule causes Imandra to look for matches of the lhs,
replacing the matched term with the (suitably instantiated) rhs, provided that
Imandra can establish ("relieve") the (suitably instantiated) hypotheses of the
rule.
For example, consider the lemma rev_len below. This lemma expresses the fact
that the length of a list x is equal to the length of List.rev x, i.e., if
we reverse a list, we end up with a list of the same length. This rule is
unconditional: it has no hypotheses. Thus, it will always be able to fire on
terms that match its left-hand side. Notice that Imandra uses a previously
defined rewrite rule in order to prove this lemma! The lemma rev_len would
make an excellent rewrite rule, so we use the [@@rw] annotation to install it:
In [17]:
lemma rev_len x =
List.length (List.rev x) = List.length x
[@@auto] [@@rw]
Out[17]:
val rev_len : 'a list -> bool = <fun> Goal: List.length (List.rev x) = List.length x. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length (List.rev x) = List.length x Verified up to bound 10 (after 0.020s). Must try induction. The recursive terms in the conjecture suggest 2 inductions. Subsumption and merging reduces this to 1. We shall induct according to a scheme derived from List.length. Induction scheme: (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x). 2 nontautological subgoals. Subgoal 1.2: H0. x = [] |--------------------------------------------------------------------------- List.length (List.rev x) = List.length x But simplification reduces this to true, using the definitions of List.length and List.rev. Subgoal 1.1: H0. not (x = []) H1. List.length (List.rev (List.tl x)) = List.length (List.tl x) |--------------------------------------------------------------------------- List.length (List.rev x) = List.length x This simplifies, using the definitions of List.length and List.rev to: Subgoal 1.1': H0. List.length (List.rev (List.tl x)) = List.length (List.tl x) H1. x <> [] |--------------------------------------------------------------------------- List.length (List.append (List.rev (List.tl x)) [List.hd x]) = 1 + List.length (List.tl x) But simplification reduces this to true, using the definition of List.length, and the rewrite rule len_append.
Proved
proof
| ground_instances | 0 |
| definitions | 7 |
| inductions | 1 |
| search_time | 0.149s |
Expand
start[0.149s, "Goal"] List.length (List.rev :var_0:) = List.length :var_0:
subproof
List.length (List.rev x) = List.length xstart[0.149s, "1"] List.length (List.rev x) = List.length x
induction on (functional ) :scheme (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x)
Split ((not (x = []) || List.length (List.rev x) = List.length x) && (not (not (x = []) && List.length (List.rev (List.tl x)) = List.length (List.tl x)) || List.length (List.rev x) = List.length x) :cases [not (x = []) || List.length (List.rev x) = List.length x; (x = [] || not (List.length (List.rev (List.tl x)) = List.length (List.tl x))) || List.length (List.rev x) = List.length x])subproof
(x = [] || not (List.length (List.rev (List.tl x)) = List.length (List.tl x))) || List.length (List.rev x) = List.length xstart[0.114s, "1.1"] (x = [] || not (List.length (List.rev (List.tl x)) = List.length (List.tl x))) || List.length (List.rev x) = List.length x
simplify
into (List.length (List.append (List.rev (List.tl x)) [List.hd x]) = 1 + List.length (List.tl x) || not (List.length (List.rev (List.tl x)) = List.length (List.tl x))) || x = []
expansions [List.length, List.rev]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
simplify
into true
expansions [List.length, List.length]
rewrite_steps len_append
forward_chaining List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
subproof
not (x = []) || List.length (List.rev x) = List.length xstart[0.114s, "1.2"] not (x = []) || List.length (List.rev x) = List.length x
simplify
into true
expansions [List.length, List.length, List.rev]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
List.len_nonnegative
len_non_neg
Loading..
With this rule installed and enabled, if Imandra's simplifier encounters a term
of the form List.length (List.rev <term>), it will replace it with the simpler
form List.length <term>.
Both the hypotheses and rhs can be omitted, in which case Imandra will default
them to true. That is, h_1 && ... && h_k ==> lhs is equivalent to
h_1 && h_k ==> lhs = true and lhs = rhs is equal to true ==> lhs = rhs.
Imandra's rewriting is:
conditional: rewrite rules may contain conditions (hypotheses), and eligible rules are only applied when their hypotheses are established. Once the pattern of a rule has been matched, Imandra uses backward-chaining ("backchaining") to relieve the rule's hypotheses, recursively attempting to simplify them to
truemodulo the current simplification context. This is important to keep in mind when developing your theories: rewrite rules will not fire unless Imandra can simplify their instantiated hypotheses totrue.oriented: given a rule whose conclusion is of the form
lhs = rhs, rewriting happens by replacing the (instantiated)lhswith the (instantiated)rhs.
When adding a new rewrite rule, users should take care to orient the equality so
that rhs is simpler or more canonical than lhs. If it's not clear what
it means for an rhs to be "better" than the lhs, e.g., in the case of the
proof for the associativity of append x @ (y @ z) = (x @ y) @ z, a canonical
form should typically be chosen (e.g., associating to the left in this case)
and kept in mind for further rules.
By default, the lhs must contain all the top-level variables of the theorem
(i.e. the arguments to the lambda term representing the goal). There is an
exception to this rule: if the lhs does not contain all the variables of the
theorem but the rule hypotheses have subterms containing the remaining free
variables, these terms can be annotated with [@trigger rw], signaling Imandra
that the annotated terms should be used to complete the matching.
It's helpful to see an example where the use of [@trigger rw] is necessary.
Let's first define a subset function on lists:
In [18]:
let rec subset x y =
match x with
| [] -> true
| x :: xs ->
if List.mem x y then subset xs y
else false
Out[18]:
val subset : 'a list -> 'a list -> bool = <fun>
termination proof
Termination proof
call `subset (List.tl x) y` from `subset x y`
| original | subset x y | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | subset (List.tl x) y | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (Ordinal.count x) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (List.tl x)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [List.mem (List.hd x) y && not (x = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
Let's now suppose that we want to verify the transitivity of subset:
In [19]:
#max_induct 1;;
verify (fun x y z -> subset x y && subset y z ==> subset x z) [@@auto]
Out[19]:
- : 'a list -> 'a list -> 'a list -> bool = <fun> Goal: subset x y && subset y z ==> subset x z. 1 nontautological subgoal. Subgoal 1: H0. subset x y H1. subset y z |--------------------------------------------------------------------------- subset x z Verified up to bound 10 (after 0.017s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from subset. Induction scheme: (not (List.mem (List.hd x) y && not (x = [])) ==> φ z y x) && (not (x = []) && List.mem (List.hd x) y && φ z y (List.tl x) ==> φ z y x). 2 nontautological subgoals. Subgoal 1.2: H0. subset x y H1. subset y z |--------------------------------------------------------------------------- C0. List.mem (List.hd x) y && not (x = []) C1. subset x z This simplifies, using the definition of subset to: Subgoal 1.2': H0. subset y z H1. subset x y |--------------------------------------------------------------------------- C0. subset x z C1. List.mem (List.hd x) y But simplification reduces this to true, using the definition of subset. Subgoal 1.1: H0. not (x = []) H1. List.mem (List.hd x) y H2. subset (List.tl x) y && subset y z ==> subset (List.tl x) z H3. subset x y H4. subset y z |--------------------------------------------------------------------------- subset x z This simplifies, using the definition of subset to: Subgoal 1.1': H0. subset y z H1. subset (List.tl x) z H2. subset (List.tl x) y H3. List.mem (List.hd x) y H4. x <> [] |--------------------------------------------------------------------------- List.mem (List.hd x) z Verified up to bound 10 (after 0.016s). We can eliminate destructors by the following substitution: x -> x1 :: x2 This produces the modified subgoal: Subgoal 1.1'': H0. subset y z H1. subset x2 z H2. subset x2 y H3. List.mem x1 y |--------------------------------------------------------------------------- List.mem x1 z Verified up to bound 10 (after 0.016s). Must try induction. Checkpoints: H0. subset y z H1. subset x2 z H2. subset x2 y H3. List.mem x1 y |--------------------------------------------------------------------------- List.mem x1 z Error: Maximum induction depth reached (1). You can set this with #max_induct.
It looks like Imandra needs an additional lemma in order to prove this. By
inspecting the checkpoint, it looks like all we need is a rule relating subset
and List.mem. Let's attempt to prove it:
In [20]:
lemma mem_subset x y z =
List.mem x y && subset y z ==> List.mem x z
[@@auto] [@@rewrite]
Out[20]:
val mem_subset : 'a -> 'a list -> 'a list -> bool = <fun> Goal: List.mem x y && subset y z ==> List.mem x z. 1 nontautological subgoal. Subgoal 1: H0. List.mem x y H1. subset y z |--------------------------------------------------------------------------- List.mem x z Verified up to bound 10 (after 0.015s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. However, scheme scoring gives us a clear winner. We shall induct according to a scheme derived from List.mem. Induction scheme: (y = [] ==> φ z y x) && (not (y = []) && φ z (List.tl y) x ==> φ z y x). 2 nontautological subgoals. Subgoal 1.2: H0. y = [] H1. List.mem x y H2. subset y z |--------------------------------------------------------------------------- List.mem x z But simplification reduces this to true, using the definition of List.mem. Subgoal 1.1: H0. not (y = []) H1. List.mem x (List.tl y) && subset (List.tl y) z ==> List.mem x z H2. List.mem x y H3. subset y z |--------------------------------------------------------------------------- List.mem x z But simplification reduces this to true, using the definitions of List.mem and subset. File "jupyter cell 20", line 1, characters 6-91: Error: in rewrite rule, variable (y : 'a list) does not occur in left-hand side of the rule or in `[@trigger rw]` terms
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.111s |
Expand
start[0.111s, "Goal"] List.mem :var_0: :var_1: && subset :var_1: :var_2: ==> List.mem :var_0: :var_2:
subproof
(not (List.mem x y) || not (subset y z)) || List.mem x zstart[0.111s, "1"] (not (List.mem x y) || not (subset y z)) || List.mem x z
induction on (functional ) :scheme (y = [] ==> φ z y x) && (not (y = []) && φ z (List.tl y) x ==> φ z y x)Split ((((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z) && (((not (not (y = []) && ((not (List.mem x (List.tl y)) || not (subset (List.tl y) z)) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z) :cases [((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z; (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z])subproof
(((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x zstart[0.065s, "1.1"] (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x zsimplify
into true
expansions [subset, List.mem, subset, List.mem]
rewrite_steps forward_chaining
subproof
((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x zstart[0.065s, "1.2"] ((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z
simplify
into true
expansions List.mem
rewrite_steps forward_chaining
Loading..
While Imandra was successful in proving this lemma, it raised an error while
trying to turn this lemma into a rewrite rule. As Imandra tells us, this is
because the free variable y does not appear in the lhs term List.mem x z.
If we, however, annotate the subset y z term with the appropriate [@trigger
rw] attribute, Imandra can then successfully turn this term into a valid
rewrite rule:
In [21]:
lemma mem_subset x y z =
List.mem x y && (subset y z [@trigger rw]) ==> List.mem x z
[@@auto] [@@rewrite]
Out[21]:
val mem_subset : 'a -> 'a list -> 'a list -> bool = <fun> Goal: List.mem x y && subset y z ==> List.mem x z. 1 nontautological subgoal. Subgoal 1: H0. List.mem x y H1. subset y z |--------------------------------------------------------------------------- List.mem x z Verified up to bound 10 (after 0.015s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. However, scheme scoring gives us a clear winner. We shall induct according to a scheme derived from List.mem. Induction scheme: (y = [] ==> φ x z y) && (not (y = []) && φ x z (List.tl y) ==> φ x z y). 2 nontautological subgoals. Subgoal 1.2: H0. y = [] H1. List.mem x y H2. subset y z |--------------------------------------------------------------------------- List.mem x z But simplification reduces this to true, using the definition of List.mem. Subgoal 1.1: H0. not (y = []) H1. List.mem x (List.tl y) && subset (List.tl y) z ==> List.mem x z H2. List.mem x y H3. subset y z |--------------------------------------------------------------------------- List.mem x z But simplification reduces this to true, using the definitions of List.mem and subset.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.114s |
Expand
start[0.114s, "Goal"] List.mem :var_0: :var_1: && subset :var_1: :var_2: ==> List.mem :var_0: :var_2:
subproof
(not (List.mem x y) || not (subset y z)) || List.mem x zstart[0.114s, "1"] (not (List.mem x y) || not (subset y z)) || List.mem x z
induction on (functional ) :scheme (y = [] ==> φ x z y) && (not (y = []) && φ x z (List.tl y) ==> φ x z y)Split ((((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z) && (((not (not (y = []) && ((not (List.mem x (List.tl y)) || not (subset (List.tl y) z)) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z) :cases [((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z; (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z])subproof
(((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x zstart[0.064s, "1.1"] (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x zsimplify
into true
expansions [subset, List.mem, subset, List.mem]
rewrite_steps forward_chaining
subproof
((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x zstart[0.064s, "1.2"] ((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z
simplify
into true
expansions List.mem
rewrite_steps forward_chaining
Loading..
And finally, let's verify that the rewrite rule can indeed match as we expect:
In [22]:
verify (fun x y z -> subset x y && subset y z ==> subset x z) [@@auto]
Out[22]:
- : 'a list -> 'a list -> 'a list -> bool = <fun> Goal: subset x y && subset y z ==> subset x z. 1 nontautological subgoal. Subgoal 1: H0. subset x y H1. subset y z |--------------------------------------------------------------------------- subset x z Verified up to bound 10 (after 0.018s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from subset. Induction scheme: (not (List.mem (List.hd x) y && not (x = [])) ==> φ z y x) && (not (x = []) && List.mem (List.hd x) y && φ z y (List.tl x) ==> φ z y x). 2 nontautological subgoals. Subgoal 1.2: H0. subset x y H1. subset y z |--------------------------------------------------------------------------- C0. List.mem (List.hd x) y && not (x = []) C1. subset x z This simplifies, using the definitions of List.mem and subset, and the rewrite rule mem_subset to: Subgoal 1.2': H0. subset y z H1. subset x y |--------------------------------------------------------------------------- C0. subset x z C1. List.mem (List.hd x) y But simplification reduces this to true, using the definition of subset. Subgoal 1.1: H0. not (x = []) H1. List.mem (List.hd x) y H2. subset (List.tl x) y && subset y z ==> subset (List.tl x) z H3. subset x y H4. subset y z |--------------------------------------------------------------------------- subset x z But simplification reduces this to true, using the definitions of List.mem and subset, and the rewrite rule mem_subset.
Proved
proof
| ground_instances | 0 |
| definitions | 9 |
| inductions | 1 |
| search_time | 0.481s |
Expand
start[0.481s, "Goal"] subset :var_0: :var_1: && subset :var_1: :var_2: ==> subset :var_0: :var_2:
subproof
(not (subset x y) || not (subset y z)) || subset x zstart[0.481s, "1"] (not (subset x y) || not (subset y z)) || subset x z
induction on (functional ) :scheme (not (List.mem (List.hd x) y && not (x = [])) ==> φ z y x) && (not (x = []) && List.mem (List.hd x) y && φ z y (List.tl x) ==> φ z y x)Split ((((List.mem (List.hd x) y && not (x = []) || not (subset x y)) || not (subset y z)) || subset x z) && (((not ((not (x = []) && List.mem (List.hd x) y) && ((not (subset (List.tl x) y) || not (subset y z)) || subset (List.tl x) z)) || not (subset x y)) || not (subset y z)) || subset x z) :cases [((not (subset x y) || not (subset y z)) || List.mem (List.hd x) y && not (x = [])) || subset x z; ((((x = [] || not (List.mem (List.hd x) y)) || not (not (subset (List.tl x) y && subset y z) || subset (List.tl x) z)) || not (subset x y)) || not (subset y z)) || subset x z])subproof
((((x = [] || not (List.mem (List.hd x) y)) || not (not (subset (List.tl x) y && subset y z) || subset (List.tl x) z)) || not (subset x y)) || not (subset y z)) || subset x zstart[0.391s, "1.1"] ((((x = [] || not (List.mem (List.hd x) y)) || not (not (subset (List.tl x) y && subset y z) || subset (List.tl x) z)) || not (subset x y)) || not (subset y z)) || subset x zsimplify
into true
expansions [subset, subset, subset, List.mem]
rewrite_steps mem_subset
mem_subset
forward_chaining
subproof
((not (subset x y) || not (subset y z)) || List.mem (List.hd x) y && not (x = [])) || subset x zstart[0.391s, "1.2"] ((not (subset x y) || not (subset y z)) || List.mem (List.hd x) y && not (x = [])) || subset x z
simplify
into ((subset x z || List.mem (List.hd x) y) || not (subset y z)) || not (subset x y)
expansions [subset, List.mem, List.mem]
rewrite_steps mem_subset
forward_chaining simplify
into true
expansions [subset, subset]
rewrite_steps forward_chaining
Loading..
Forward-chaining Rules¶
Forward chaining is the second type of rule that Imandra allows us to register and participate automatically in proofs.
A forward chaining rule is a theorem containing a collection of trigger terms which must include all free variables of the theorem. If Imandra can appropriately match the triggers with terms in the goal, then an instantiation of the rule is added to the context. The context of a goal is not displayed in the goal itself (i.e., when the goal is printed), but is rather used in the background to aid the simplifier in closing branches, relieving hypotheses of rewrite rules during backchaining, and so on.
For example, let us prove the following theorem and install it as a forward-chaining rule:
In [23]:
lemma len_nonnegative x =
List.length x [@trigger] >= 0
[@@simp] [@@fc]
Out[23]:
val len_nonnegative : 'a list -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 0 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.040s | ||||||||||||
| details | Expand
|
Expand
start[0.040s] List.length :var_0: >= 0
simplify
into true
expansions []
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
Now when Imandra encounters a term of the form List.length <term>, the formula
List.length <term> >= 0 will be added to the context of the goal under
focus. In other words, a forward chaining rule allows Imandra to extend the
database of background logical facts it knows about a goal. These facts are made
available to the simplifier, and can thus be used to enhance simplification by
closing branches and relieving hypotheses of conditional rewrite rules.
A forward chaining rule can contain multiple disjoint triggers. In this case, if
either of the triggers matches, the forward chaining rule fires. For example,
the following forward chaining version of the rev_len rewrite rule we added
above will fire if either List.length x or List.length (List.rev x)
matches.
In [24]:
lemma rev_len_fc x =
List.length x [@trigger] = List.length (List.rev x) [@trigger]
[@@auto] [@@fc]
Out[24]:
val rev_len_fc : 'a list -> bool = <fun> Goal: List.length x = List.length (List.rev x). 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length x = List.length (List.rev x) But simplification reduces this to true, using the rewrite rule rev_len.
Proved
proof
| ground_instances | 0 |
| definitions | 0 |
| inductions | 0 |
| search_time | 0.010s |
Expand
start[0.010s, "Goal"] List.length :var_0: = List.length (List.rev :var_0:)
subproof
List.length x = List.length (List.rev x)start[0.009s, "1"] List.length x = List.length (List.rev x)
simplify
into true
expansions []
rewrite_steps rev_len
forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
List.len_nonnegative
len_non_neg
len_nonnegative
Loading..
Additionally, a forward chaining rule can contain multiple conjoined triggers, forming a trigger cluster. In this case, all the triggers must match in order for the forward chaining rule to apply.
To create a trigger cluster multiple terms must be annotated with
[@trigger <x>n], where <x> is a numeric identifier common to all
the triggers in the cluster. For example:
In [25]:
theorem subset_trans l1 l2 l3 =
(subset l1 l2 [@trigger 0n]) && (subset l2 l3 [@trigger 0n])
==>
subset l1 l3
[@@auto] [@@forward_chaining]
Out[25]:
val subset_trans : 'a list -> 'a list -> 'a list -> bool = <fun> Goal: subset l1 l2 && subset l2 l3 ==> subset l1 l3. 1 nontautological subgoal. Subgoal 1: H0. subset l1 l2 H1. subset l2 l3 |--------------------------------------------------------------------------- subset l1 l3 Verified up to bound 10 (after 0.016s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from subset. Induction scheme: (not (List.mem (List.hd l1) l2 && not (l1 = [])) ==> φ l3 l2 l1) && (not (l1 = []) && List.mem (List.hd l1) l2 && φ l3 l2 (List.tl l1) ==> φ l3 l2 l1). 2 nontautological subgoals. Subgoal 1.2: H0. subset l1 l2 H1. subset l2 l3 |--------------------------------------------------------------------------- C0. List.mem (List.hd l1) l2 && not (l1 = []) C1. subset l1 l3 This simplifies, using the definitions of List.mem and subset, and the rewrite rule mem_subset to: Subgoal 1.2': H0. subset l2 l3 H1. subset l1 l2 |--------------------------------------------------------------------------- C0. subset l1 l3 C1. List.mem (List.hd l1) l2 But simplification reduces this to true, using the definition of subset. Subgoal 1.1: H0. not (l1 = []) H1. List.mem (List.hd l1) l2 H2. subset (List.tl l1) l2 && subset l2 l3 ==> subset (List.tl l1) l3 H3. subset l1 l2 H4. subset l2 l3 |--------------------------------------------------------------------------- subset l1 l3 But simplification reduces this to true, using the definitions of List.mem and subset, and the rewrite rule mem_subset.
Proved
proof
| ground_instances | 0 |
| definitions | 9 |
| inductions | 1 |
| search_time | 0.475s |
Expand
start[0.475s, "Goal"] subset :var_0: :var_1: && subset :var_1: :var_2: ==> subset :var_0: :var_2:
subproof
(not (subset l1 l2) || not (subset l2 l3)) || subset l1 l3start[0.475s, "1"] (not (subset l1 l2) || not (subset l2 l3)) || subset l1 l3
induction on (functional ) :scheme (not (List.mem (List.hd l1) l2 && not (l1 = [])) ==> φ l3 l2 l1) && (not (l1 = []) && List.mem (List.hd l1) l2 && φ l3 l2 (List.tl l1) ==> φ l3 l2 l1)Split ((((List.mem (List.hd l1) l2 && not (l1 = []) || not (subset l1 l2)) || not (subset l2 l3)) || subset l1 l3) && (((not ((not (l1 = []) && List.mem (List.hd l1) l2) && ((not (subset (List.tl l1) l2) || not (subset l2 l3)) || subset (List.tl l1) l3)) || not (subset l1 l2)) || not (subset l2 l3)) || subset l1 l3) :cases [((not (subset l1 l2) || not (subset l2 l3)) || List.mem (List.hd l1) l2 && not (l1 = [])) || subset l1 l3; ((((l1 = [] || not (List.mem (List.hd l1) l2)) || not (not (subset (List.tl l1) l2 && subset l2 l3) || subset (List.tl l1) l3)) || not (subset l1 l2)) || not (subset l2 l3)) || subset l1 l3])subproof
((((l1 = [] || not (List.mem (List.hd l1) l2)) || not (not (subset (List.tl l1) l2 && subset l2 l3) || subset (List.tl l1) l3)) || not (subset l1 l2)) || not (subset l2 l3)) || subset l1 l3start[0.392s, "1.1"] ((((l1 = [] || not (List.mem (List.hd l1) l2)) || not (not (subset (List.tl l1) l2 && subset l2 l3) || subset (List.tl l1) l3)) || not (subset l1 l2)) || not (subset l2 l3)) || subset l1 l3simplify
into true
expansions [subset, subset, subset, List.mem]
rewrite_steps mem_subset
mem_subset
forward_chaining
subproof
((not (subset l1 l2) || not (subset l2 l3)) || List.mem (List.hd l1) l2 && not (l1 = [])) || subset l1 l3start[0.392s, "1.2"] ((not (subset l1 l2) || not (subset l2 l3)) || List.mem (List.hd l1) l2 && not (l1 = [])) || subset l1 l3
simplify
into ((subset l1 l3 || List.mem (List.hd l1) l2) || not (subset l2 l3)) || not (subset l1 l2)
expansions [subset, List.mem, List.mem]
rewrite_steps mem_subset
forward_chaining simplify
into true
expansions [subset, subset]
rewrite_steps forward_chaining
Loading..
This forward chaining rule will match only if a goal contains terms that match
both subset l1 l2 and subset l2 l3.
It should be noted that Imandra supports automatic trigger selection, meaning it's often not necessary to annotate the trigger terms manually. Imandra can typically infer for us both simple triggers and trigger clusters. In fact for both the single trigger examples above, we could have omitted the trigger annotations altogether, and Imandra would have found some for us automatically.
Blast¶
Sometimes, Unrolling gets lost in the search space. Imandra has an alternative strategy called blast, that can be invoked in any context where unrolling is accepted:
In [26]:
verify (fun a b -> a >= 0 && b >= 0 && a <= 1_000 && b <= 1_000 ==> (a-b) * (a-b) * (b-a) * (b-a) + 1 >= 0) [@@blast];;
Out[26]:
- : int -> int -> bool = <fun>
proof from "blast" (after 0.20s)!
Proved
blast is usually handy in problems that present some form of combinatorial explosion. A more detailed example shows how to solve a sudoku with Imandra, and how to cross a river safely.
Blast is our name for a symbolic execution technique for Imandra's core logic of recursive functions and algebraic datatypes. The way it works is by exploring progressively the space of its inputs (e.g. lists of size 0, then size 1, then size 2, etc.) and encoding the computations into SAT by executing "simultaneously" all possible paths. It views all logic-mode definitions through the prism of computation — blast doesn't know that x = x is always true, for example, it will try to expand x progressively and computing the predicate x = x as it goes.
This means that [@@blast] shines when there's a counter-example (or instance) to find: expanding the input(s) progressively and computing whether the goal holds is exactly what [@@blast] is designed for. On the other hand, if you're trying to prove a theorem about List.rev (List.rev x) = x, the space of possible values for x is infinite and [@@blast] will never be able to explore it all. Induction is generally more adequate for proving such universal statements. Conversely, to solve a sudoku, it's appropriate to explore the space of sudoku grids s until one is found that satisfies is_sudoku s && is_solution_of s the_initial_grid (meaning this expression evaluates to true).
Induction¶
While techniques such as unrolling and simplification can get us a long way towards formally verifying our software, variants of mathematical induction are in general required for verifying properties of systems with infinite state-spaces.
Induction is a proof technique that can be used to prove that some property
φ(x) holds for all the elements x of a recursively defined structure (e.g.
natural numbers, lists, trees, execution traces, etc). The proof consists of:
- a proof that
φ(base)is true for each base case - a proof that if
φ(c)is true (called the inductive hypothesis), thenφ(step(c))is also true, for all the recursive steps of the property we're trying to prove
Induction can be done in many ways, and finding the "right" way to induct is often the key to difficult problems. Imandra has deep automation for finding and applying the "right" induction for a problem. If this fails, the user can instruct Imandra how to induct, with various forms of instructions.
A method of induction is given by an induction scheme.
Induction schemes can automatically be derived by Imandra in many ways. By
default, with [@@auto] or [@@induct], Imandra analyses the recursive
functions involved in the conjecture and constructs a functional induction
scheme derived from their recursive structure, in a manner that is justified by
the ordinal measures used to prove their termination. Imandra also supports
structural induction principles derived from the definitions of (well-founded)
algebraic datatypes such as lists and trees.
Some example induction schemes are:
- for the natural numbers,
φ(Zero) && φ(n) ==> φ(Succ(n)) - for lists,
φ([]) && (lst <> [] && φ(List.tl(lst)) ==> φ (lst)) - for the function
repeatas defined below,n <= 0 ==> φ(n, c) && (n > 0 && φ(n - 1, c)) ==> φ(n, c)
In [27]:
let rec repeat c n =
if n <= 0 then
[]
else
c :: (repeat c (n-1))
Out[27]:
val repeat : 'a -> int -> 'a list = <fun>
termination proof
Termination proof
call `repeat c (n - 1)` from `repeat c n`
| original | repeat c n | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | repeat c (n - 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if n >= 0 then n else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (n <= 0)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
In Imandra, induction schemes are "destructor style." So, an actual scheme
Imandra would produce for a goal involving n : nat (where type nat = Zero | Succ of nat)
is:
(n = Zero ==> φ n)
&& (not (n = Zero) && φ (Destruct(Succ, 0, n)) ==> φ n).Let us see a few example inductions.
In [28]:
lemma assoc_append x y z =
x @ (y @ z) = (x @ y) @ z [@@auto] [@@rw]
Out[28]:
val assoc_append : 'a list -> 'a list -> 'a list -> bool = <fun> Goal: x @ y @ z = (x @ y) @ z. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.append x (List.append y z) = List.append (List.append x y) z Verified up to bound 10 (after 0.021s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from List.append. Induction scheme: (x = [] ==> φ z y x) && (not (x = []) && φ z y (List.tl x) ==> φ z y x). 2 nontautological subgoals. Subgoal 1.2: H0. x = [] |--------------------------------------------------------------------------- List.append x (List.append y z) = List.append (List.append x y) z But simplification reduces this to true, using the definition of List.append. Subgoal 1.1: H0. not (x = []) H1. List.append (List.tl x) (List.append y z) = List.append (List.append (List.tl x) y) z |--------------------------------------------------------------------------- List.append x (List.append y z) = List.append (List.append x y) z But simplification reduces this to true, using the definition of List.append.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.057s |
Expand
start[0.057s, "Goal"] List.append :var_0: (List.append :var_1: :var_2:) = List.append (List.append :var_0: :var_1:) :var_2:
subproof
List.append x (List.append y z) = List.append (List.append x y) zstart[0.057s, "1"] List.append x (List.append y z) = List.append (List.append x y) z
induction on (functional ) :scheme (x = [] ==> φ z y x) && (not (x = []) && φ z y (List.tl x) ==> φ z y x)Split ((not (x = []) || List.append x (List.append y z) = List.append (List.append x y) z) && (not (not (x = []) && List.append (List.tl x) (List.append y z) = List.append (List.append (List.tl x) y) z) || List.append x (List.append y z) = List.append (List.append x y) z) :cases [not (x = []) || List.append x (List.append y z) = List.append (List.append x y) z; (x = [] || not (List.append (List.tl x) (List.append y z) = List.append (List.append (List.tl x) y) z)) || List.append x (List.append y z) = List.append (List.append x y) z])subproof
(x = [] || not (List.append (List.tl x) (List.append y z) = List.append (List.append (List.tl x) y) z)) || List.append x (List.append y z) = List.append (List.append x y) zstart[0.025s, "1.1"] (x = [] || not (List.append (List.tl x) (List.append y z) = List.append (List.append (List.tl x) y) z)) || List.append x (List.append y z) = List.append (List.append x y) zsimplify
into true
expansions [List.append, List.append, List.append]
rewrite_steps forward_chaining
subproof
not (x = []) || List.append x (List.append y z) = List.append (List.append x y) zstart[0.025s, "1.2"] not (x = []) || List.append x (List.append y z) = List.append (List.append x y) z
simplify
into true
expansions [List.append, List.append]
rewrite_steps forward_chaining
Loading..
In [29]:
lemma rev_append x y =
List.rev (x @ y) = List.rev y @ List.rev x
[@@auto]
Out[29]:
val rev_append : 'a list -> 'a list -> bool = <fun> Goal: List.rev (x @ y) = List.rev y @ List.rev x. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.rev (List.append x y) = List.append (List.rev y) (List.rev x) Verified up to bound 10 (after 0.019s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from List.append. Induction scheme: (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x). 2 nontautological subgoals. Subgoal 1.2: H0. x = [] |--------------------------------------------------------------------------- List.rev (List.append x y) = List.append (List.rev y) (List.rev x) But simplification reduces this to true, using the definitions of List.append and List.rev, and the rewrite rule List.append_to_nil. Subgoal 1.1: H0. not (x = []) H1. List.rev (List.append (List.tl x) y) = List.append (List.rev y) (List.rev (List.tl x)) |--------------------------------------------------------------------------- List.rev (List.append x y) = List.append (List.rev y) (List.rev x) This simplifies, using the definitions of List.append and List.rev to: Subgoal 1.1': H0. List.rev (List.append (List.tl x) y) = List.append (List.rev y) (List.rev (List.tl x)) H1. x <> [] |--------------------------------------------------------------------------- List.append (List.rev (List.append (List.tl x) y)) [List.hd x] = List.append (List.rev y) (List.append (List.rev (List.tl x)) [List.hd x]) But simplification reduces this to true, using the rewrite rule assoc_append.
Proved
proof
| ground_instances | 0 |
| definitions | 6 |
| inductions | 1 |
| search_time | 0.231s |
Expand
start[0.231s, "Goal"] List.rev (List.append :var_0: :var_1:) = List.append (List.rev :var_1:) (List.rev :var_0:)
subproof
List.rev (List.append x y) = List.append (List.rev y) (List.rev x)start[0.231s, "1"] List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
induction on (functional ) :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
Split ((not (x = []) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)) && (not (not (x = []) && List.rev (List.append (List.tl x) y) = List.append (List.rev y) (List.rev (List.tl x))) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)) :cases [not (x = []) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x); (x = [] || not (List.rev (List.append (List.tl x) y) = List.append (List.rev y) (List.rev (List.tl x)))) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)])subproof
(x = [] || not (List.rev (List.append (List.tl x) y) = List.append (List.rev y) (List.rev (List.tl x)))) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)start[0.184s, "1.1"] (x = [] || not (List.rev (List.append (List.tl x) y) = List.append (List.rev y) (List.rev (List.tl x)))) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)simplify
into (List.append (List.rev (List.append (List.tl x) y)) [List.hd x] = List.append (List.rev y) (List.append (List.rev (List.tl x)) [List.hd x]) || not (List.rev (List.append (List.tl x) y) = List.append (List.rev y) (List.rev (List.tl x)))) || x = []expansions [List.rev, List.rev, List.append]
rewrite_steps forward_chaining simplify
into true
expansions []
rewrite_steps assoc_append
forward_chaining
subproof
not (x = []) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)start[0.184s, "1.2"] not (x = []) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
simplify
into true
expansions [List.append, List.rev, List.append]
rewrite_steps List.append_to_nil
forward_chaining
Loading..
In [30]:
verify (fun lst ->
List.for_all (fun x -> x > 0) lst ==>
List.fold_right (+) ~base:1 lst > 0)
[@@auto]
Out[30]:
- : int list -> bool = <fun> Goal: List.for_all (fun x -> x > 0) lst ==> List.fold_right + 1 lst > 0. 1 nontautological subgoal. Subgoal 1: H0. List.for_all (fun x -> x > 0) lst H1. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false Verified up to bound 10 (after 0.020s). Must try induction. The recursive terms in the conjecture suggest 2 inductions. Subsumption and merging reduces this to 1. We shall induct according to a scheme derived from List.for_all. Induction scheme: (lst = [] ==> φ lst) && (not (lst = []) && φ (List.tl lst) ==> φ lst). 2 nontautological subgoals. Subgoal 1.2: H0. lst = [] H1. List.for_all (fun x -> x > 0) lst H2. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definitions of List.fold_right and List.for_all. Subgoal 1.1: H0. not (lst = []) H1. not (List.for_all (fun x -> x > 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0) H2. List.for_all (fun x -> x > 0) lst H3. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definitions of List.fold_right and List.for_all.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.077s |
Expand
start[0.077s, "Goal"] List.for_all (fun x -> x > 0) :var_0: ==> List.fold_right + 1 :var_0: > 0
subproof
not (List.for_all (fun x -> x > 0) lst) || not (List.fold_right + 1 lst <= 0)start[0.077s, "1"] not (List.for_all (fun x -> x > 0) lst) || not (List.fold_right + 1 lst <= 0)
induction on (functional ) :scheme (lst = [] ==> φ lst) && (not (lst = []) && φ (List.tl lst) ==> φ lst)Split (((not (lst = []) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)) && ((not (not (lst = []) && (not (List.for_all (fun x -> x > 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)) :cases [(not (lst = []) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0); ((lst = [] || not (not (List.for_all (fun x -> x > 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)])subproof
((lst = [] || not (not (List.for_all (fun x -> x > 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)start[0.042s, "1.1"] ((lst = [] || not (not (List.for_all (fun x -> x > 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)simplify
into true
expansions [List.for_all, List.fold_right, List.for_all]
rewrite_steps forward_chaining
subproof
(not (lst = []) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)start[0.042s, "1.2"] (not (lst = []) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)
simplify
into true
expansions [List.fold_right, List.for_all]
rewrite_steps forward_chaining
Loading..
Functional Induction¶
By default, Imandra uses functional induction (also known as recursion induction).
A functional induction scheme is one derived from the recursive structure of a function definition. The termination measure used to admit the function is also used to justify the soundness of the functional induction scheme. Unless instructed otherwise, Imandra will consider all recursive functions in a goal, analyse their recursions and instances, and apply various heuristics to merge and score them and adapt them to the conjecture being proved. In general, there may be more than one plausible induction scheme to choose from, and selecting the "right" way to induct can often be a key step in difficult proofs. Imandra will often make the "right" decision. However, in case it doesn't, it is also possible to manually specify the induction that Imandra should do.
Let us return to the function repeat above and see functional induction in
action.
In [31]:
lemma repeat_len c n =
n >= 0 ==>
List.length (repeat c n) = n [@@auto]
Out[31]:
val repeat_len : 'a -> int -> bool = <fun> Goal: n >= 0 ==> List.length (repeat c n) = n. 1 nontautological subgoal. Subgoal 1: H0. n >= 0 |--------------------------------------------------------------------------- List.length (repeat c n) = n Verified up to bound 10 (after 0.021s). Must try induction. We shall induct according to a scheme derived from repeat. Induction scheme: (n <= 0 ==> φ n c) && (not (n <= 0) && φ (n - 1) c ==> φ n c). 2 nontautological subgoals. Subgoal 1.2: H0. n <= 0 H1. n >= 0 |--------------------------------------------------------------------------- List.length (repeat c n) = n But simplification reduces this to true, using the definitions of List.length and repeat. Subgoal 1.1: H0. not (n <= 0) H1. n >= 1 ==> List.length (repeat c (-1 + n)) = -1 + n H2. n >= 0 |--------------------------------------------------------------------------- List.length (repeat c n) = n But simplification reduces this to true, using the definitions of List.length and repeat.
Proved
proof
| ground_instances | 0 |
| definitions | 4 |
| inductions | 1 |
| search_time | 0.135s |
Expand
start[0.135s, "Goal"] :var_0: >= 0 ==> List.length (repeat :var_1: :var_0:) = :var_0:
subproof
not (n >= 0) || List.length (repeat c n) = nstart[0.134s, "1"] not (n >= 0) || List.length (repeat c n) = n
induction on (functional ) :scheme (n <= 0 ==> φ n c) && (not (n <= 0) && φ (n - 1) c ==> φ n c)
Split (((not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n) && ((not (not (n <= 0) && (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n)) || not (n >= 0)) || List.length (repeat c n) = n) :cases [(not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n; ((n <= 0 || not (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n)) || not (n >= 0)) || List.length (repeat c n) = n])subproof
((n <= 0 || not (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n)) || not (n >= 0)) || List.length (repeat c n) = nstart[0.043s, "1.1"] ((n <= 0 || not (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n)) || not (n >= 0)) || List.length (repeat c n) = n
simplify
into true
expansions [List.length, repeat]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
subproof
(not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = nstart[0.043s, "1.2"] (not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n
simplify
into true
expansions [List.length, repeat]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
Loading..
Functional induction schemes tailored to a problem can also be manually specified.
In order to manually specify a functional induction, one must define a recursive function encoding the recursion scheme one wants available in induction (Imandra doesn't care what the function does, it only looks at how it recurses). As always, Imandra must be able to prove that the recursive function terminates in order for it to be admitted into the logic. The ordinal measures used in the termination proof are then used to justify subsequent functional induction schemes derived from the function.
Let's see a simple example. Note that we could trivially prove this goal with
[@@auto], but we shall use it to illustrate the process of manual induction
schemes nevertheless! For fun, we'll make our custom induction scheme have two
base-cases.
In [32]:
let rec sum n =
if n <= 0 then 0
else n + sum (n-1)
let rec induct_scheme (n : int) =
if n <= 0 then true
else if n = 1 then true
else induct_scheme (n-1)
Out[32]:
val sum : int -> Z.t = <fun> val induct_scheme : int -> bool = <fun>
termination proof
Termination proof
call `sum (n - 1)` from `sum n`
| original | sum n | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | sum (n - 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if n >= 0 then n else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (n <= 0)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
termination proof
Termination proof
call `induct_scheme (n - 1)` from `induct_scheme n`
| original | induct_scheme n | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | induct_scheme (n - 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if n >= 0 then n else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (n = 1) && not (n <= 0)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
In [33]:
verify (fun n -> n >= 0 ==> sum n = (n * (n+1)) / 2) [@@induct functional induct_scheme]
Out[33]:
- : int -> bool = <fun> Goal: n >= 0 ==> sum n = (n * (n + 1)) / 2. 1 nontautological subgoal. Subgoal 1: H0. n >= 0 |--------------------------------------------------------------------------- sum n = (n * (1 + n)) / 2 Verified up to bound 10 (after 0.030s). Must try induction. Note: We must proceed by induction, but our current subgoal is less appropriate for induction than our original conjecture. Thus, we prefer to abandon our work until now and return our focus to the original conjecture which we shall attempt to prove by induction directly. Experimental: You are using new support for non-present functional inductions! Induction scheme: (not (not (n = 1) && not (n <= 0)) ==> φ n) && (not (n <= 0) && not (n = 1) && φ (n - 1) ==> φ n). 2 nontautological subgoals. Subgoal 2: H0. n >= 0 |--------------------------------------------------------------------------- C0. not (n = 1) && not (n <= 0) C1. sum n = (n * (1 + n)) / 2 This simplifies, using the definition of sum to: Subgoal 2': H0. n = 1 H1. n >= 0 |--------------------------------------------------------------------------- sum n = (n * (1 + n)) / 2 But simplification reduces this to true, using the definition of sum. Subgoal 1: H0. not (n <= 0) H1. not (n = 1) H2. n >= 1 ==> sum (-1 + n) = (n * (-1 + n)) / 2 H3. n >= 0 |--------------------------------------------------------------------------- sum n = (n * (1 + n)) / 2 But simplification reduces this to true, using the definition of sum.
Proved
proof
| ground_instances | 0 |
| definitions | 4 |
| inductions | 1 |
| search_time | 0.077s |
Expand
start[0.077s, "Goal"] :var_0: >= 0 ==> sum :var_0: = (:var_0: * (:var_0: + 1)) / 2
subproof
not (n >= 0) || sum n = (n * (1 + n)) / 2start[0.077s, "1"] not (n >= 0) || sum n = (n * (1 + n)) / 2
induction on (functional induct_scheme) :scheme (not (not (n = 1) && not (n <= 0)) ==> φ n) && (not (n <= 0) && not (n = 1) && φ (n - 1) ==> φ n)Split (((not (n = 1) && not (n <= 0) || not (n >= 0)) || sum n = (n * (1 + n)) / 2) && ((not ((not (n <= 0) && not (n = 1)) && (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2)) || not (n >= 0)) || sum n = (n * (1 + n)) / 2) :cases [(not (n >= 0) || not (n = 1) && not (n <= 0)) || sum n = (n * (1 + n)) / 2; (((n <= 0 || n = 1) || not (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2)) || not (n >= 0)) || sum n = (n * (1 + n)) / 2])subproof
(((n <= 0 || n = 1) || not (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2)) || not (n >= 0)) || sum n = (n * (1 + n)) / 2start[0.034s, "1"] (((n <= 0 || n = 1) || not (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2)) || not (n >= 0)) || sum n = (n * (1 + n)) / 2simplify
into true
expansions sum
rewrite_steps forward_chaining
subproof
(not (n >= 0) || not (n = 1) && not (n <= 0)) || sum n = (n * (1 + n)) / 2start[0.034s, "2"] (not (n >= 0) || not (n = 1) && not (n <= 0)) || sum n = (n * (1 + n)) / 2
simplify
into (sum n = (n * (1 + n)) / 2 || not (n = 1)) || not (n >= 0)
expansions sum
rewrite_steps forward_chaining simplify
into true
expansions [sum, sum]
rewrite_steps forward_chaining
Loading..
Note that it's rare to have to manually instruct Imandra how to induct in this
way. Usually, if you need to instruct Imandra to use a different scheme than the
one it automatically picked, you'll simply need to give Imandra the hint of
"inducting following key recursive function foo" in your goal. For example, if
Imandra had made a wrong selection in a goal involving sum and some other
recursive functions, we might tell Imandra [@@induct functional sum] to get it
to select a scheme derived from the recursive structure of sum.
Structural Induction¶
Imandra also supports structural induction. Unlike functional induction schemes which are derived from recursive functions, structural induction schemes are derived from type definitions.
For example, we can define a type of binary trees and prove a property about them by structural induction.
In [34]:
type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf
Out[34]:
type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf
In [35]:
let rec size (x : 'a tree) =
match x with
| Node (_, a,b) -> size a + size b
| Leaf -> 1
Out[35]:
val size : 'a tree -> Z.t = <fun>
termination proof
Termination proof
call `size (Destruct(Node, 1, x))` from `size x`
| original | size x | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | size (Destruct(Node, 1, x)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (Ordinal.count x) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (Destruct(Node, 1, x))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [Is_a(Node, x)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
call `size (Destruct(Node, 2, x))` from `size x`
| original | size x | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | size (Destruct(Node, 2, x)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (Ordinal.count x) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (Destruct(Node, 2, x))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [Is_a(Node, x)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
In [36]:
verify (fun x -> size x > 0) [@@induct structural x]
Out[36]:
- : 'a tree -> bool = <fun> Goal: size x > 0. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- not (size x <= 0) Verified up to bound 10 (after 0.036s). Must try induction. Induction scheme: φ Leaf && (Is_a(Node, x) && φ (Destruct(Node, 1, x)) && φ (Destruct(Node, 2, x)) ==> φ x). 2 nontautological subgoals. Subgoal 1.2: |--------------------------------------------------------------------------- not (size Leaf <= 0) But simplification reduces this to true, using the definition of size. Subgoal 1.1: H0. Is_a(Node, x) H1. not (size (Destruct(Node, 1, x)) <= 0) H2. not (size (Destruct(Node, 2, x)) <= 0) H3. size x <= 0 |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definition of size.
Proved
proof
| ground_instances | 0 |
| definitions | 2 |
| inductions | 1 |
| search_time | 0.061s |
Expand
start[0.061s, "Goal"] size :var_0: > 0
subproof
not (size x <= 0)start[0.061s, "1"] not (size x <= 0)
induction on (structural+ x) :scheme φ Leaf && (Is_a(Node, x) && φ (Destruct(Node, 1, x)) && φ (Destruct(Node, 2, x)) ==> φ x)Split (not (size Leaf <= 0) && (not ((Is_a(Node, x) && not (size (Destruct(Node, 1, x)) <= 0)) && not (size (Destruct(Node, 2, x)) <= 0)) || not (size x <= 0)) :cases [not (size Leaf <= 0); ((not Is_a(Node, x) || size (Destruct(Node, 1, x)) <= 0) || size (Destruct(Node, 2, x)) <= 0) || not (size x <= 0)])subproof
((not Is_a(Node, x) || size (Destruct(Node, 1, x)) <= 0) || size (Destruct(Node, 2, x)) <= 0) || not (size x <= 0)start[0.016s, "1.1"] ((not Is_a(Node, x) || size (Destruct(Node, 1, x)) <= 0) || size (Destruct(Node, 2, x)) <= 0) || not (size x <= 0)
simplify
into true
expansions size
rewrite_steps forward_chaining
subproof
not (size Leaf <= 0)start[0.016s, "1.2"] not (size Leaf <= 0)
simplify
into true
expansions size
rewrite_steps forward_chaining
Loading..
Structural induction comes in both additive and multiplicative flavors.
This distinction only manifests when one is performing structural induction over
multiple variables simultaneously. It affects the way base cases and inductive
steps are mixed. Let's assume one needs to do induction on x, y:
addictive structural induction gives you 3 cases: two base cases
φ(x_base, y),φ(x, y_base)and one inductive stepφ(x,y) ==> φ(step(x), step(y))multiplicative structural induction gives you 4 cases: one base case
φ(x_base, y_base)and three inductive stepsφ(x, y_base) ==> φ(step(x), y_base),φ(x_base, y) ==> φ(x_base, step(y))andφ(x,y) ==> φ(step(x), step(y))
We can see the difference using the following function:
In [37]:
let rec interleave_strict x y = match x, y with
| [], _ | _ , [] -> []
| x::xs, y::ys -> x::y::(interleave_strict xs ys)
Out[37]:
val interleave_strict : 'a list -> 'a list -> 'a list = <fun>
termination proof
Termination proof
call `interleave_strict (List.tl x) (List.tl y)` from `interleave_strict x y`
| original | interleave_strict x y | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | interleave_strict (List.tl x) (List.tl y) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (Ordinal.count x) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (List.tl x)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (x = [] || y = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
Let's prove that the length of interleave_strict x y is always less than or
equal to the sum of the lengths of x and y. We'll do it first using
additive and then using multiplicative structural induction:
In [38]:
verify (fun x y ->
List.length @@ interleave_strict x y <= List.length x + List.length y)
[@@induct structural_add (x,y)]
Out[38]:
- : 'a list -> 'a list -> bool = <fun> Goal: (List.length @@ interleave_strict x y) <= (List.length x + List.length y). 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length (interleave_strict x y) <= (List.length x + List.length y) Verified up to bound 10 (after 0.024s). Must try induction. Induction scheme: φ y [] && φ [] x && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x). 3 nontautological subgoals. Subgoal 1.3: |--------------------------------------------------------------------------- List.length (interleave_strict [] y) <= (List.length [] + List.length y) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.2: |--------------------------------------------------------------------------- List.length (interleave_strict x []) <= (List.length x + List.length []) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.1: H0. x <> [] H1. y <> [] H2. List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)) |--------------------------------------------------------------------------- List.length (interleave_strict x y) <= (List.length x + List.length y) This simplifies, using the definitions of List.length and interleave_strict to: Subgoal 1.1': H0. List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)) H1. y <> [] H2. x <> [] |--------------------------------------------------------------------------- List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <= ((1 + List.length (List.tl x)) + List.length (List.tl y)) But simplification reduces this to true, using the definition of List.length.
Proved
proof
| ground_instances | 0 |
| definitions | 11 |
| inductions | 1 |
| search_time | 0.199s |
Expand
start[0.199s, "Goal"] List.length (interleave_strict :var_0: :var_1:) <= (List.length :var_0: + List.length :var_1:)
subproof
List.length (interleave_strict x y) <= (List.length x + List.length y)start[0.199s, "1"] List.length (interleave_strict x y) <= (List.length x + List.length y)
induction on (structural+ x, y) :scheme φ y [] && φ [] x && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x)Split ((List.length (interleave_strict [] y) <= (List.length [] + List.length y) && List.length (interleave_strict x []) <= (List.length x + List.length [])) && (not ((x <> [] && y <> []) && List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y))) || List.length (interleave_strict x y) <= (List.length x + List.length y)) :cases [List.length (interleave_strict [] y) <= (List.length [] + List.length y); List.length (interleave_strict x []) <= (List.length x + List.length []); ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)])subproof
((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)start[0.155s, "1.1"] ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)simplify
into ((List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <= ((1 + List.length (List.tl x)) + List.length (List.tl y)) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || not (y <> [])) || not (x <> [])expansions [List.length, List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
simplify
into true
expansions List.length
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
subproof
List.length (interleave_strict x []) <= (List.length x + List.length [])start[0.155s, "1.2"] List.length (interleave_strict x []) <= (List.length x + List.length [])
simplify
into true
expansions [List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
subproof
List.length (interleave_strict [] y) <= (List.length [] + List.length y)start[0.155s, "1.3"] List.length (interleave_strict [] y) <= (List.length [] + List.length y)
simplify
into true
expansions [List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
Loading..
In [39]:
verify (fun x y ->
List.length @@ interleave_strict x y <= List.length x + List.length y)
[@@induct structural_mult (x,y)]
Out[39]:
- : 'a list -> 'a list -> bool = <fun> Goal: (List.length @@ interleave_strict x y) <= (List.length x + List.length y). 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length (interleave_strict x y) <= (List.length x + List.length y) Verified up to bound 10 (after 0.027s). Must try induction. Induction scheme: φ [] [] && (x <> [] && φ [] (List.tl x) ==> φ [] x) && (y <> [] && φ (List.tl y) [] ==> φ y []) && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x). 4 nontautological subgoals. Subgoal 1.4: |--------------------------------------------------------------------------- List.length (interleave_strict [] []) <= (2 * List.length []) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.3: H0. x <> [] H1. List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []) |--------------------------------------------------------------------------- List.length (interleave_strict x []) <= (List.length x + List.length []) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.2: H0. y <> [] H1. List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)) |--------------------------------------------------------------------------- List.length (interleave_strict [] y) <= (List.length [] + List.length y) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.1: H0. x <> [] H1. y <> [] H2. List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)) |--------------------------------------------------------------------------- List.length (interleave_strict x y) <= (List.length x + List.length y) This simplifies, using the definitions of List.length and interleave_strict to: Subgoal 1.1': H0. List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)) H1. y <> [] H2. x <> [] |--------------------------------------------------------------------------- List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <= ((1 + List.length (List.tl x)) + List.length (List.tl y)) But simplification reduces this to true, using the definition of List.length.
Proved
proof
| ground_instances | 0 |
| definitions | 22 |
| inductions | 1 |
| search_time | 0.243s |
Expand
start[0.243s, "Goal"] List.length (interleave_strict :var_0: :var_1:) <= (List.length :var_0: + List.length :var_1:)
subproof
List.length (interleave_strict x y) <= (List.length x + List.length y)start[0.242s, "1"] List.length (interleave_strict x y) <= (List.length x + List.length y)
induction on (structural* x, y) :scheme φ [] [] && (x <> [] && φ [] (List.tl x) ==> φ [] x) && (y <> [] && φ (List.tl y) [] ==> φ y []) && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x)Split (((List.length (interleave_strict [] []) <= (2 * List.length []) && (not (x <> [] && List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length [])) || List.length (interleave_strict x []) <= (List.length x + List.length []))) && (not (y <> [] && List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y))) && (not ((x <> [] && y <> []) && List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y))) || List.length … <= …) :cases [List.length (interleave_strict [] []) <= (2 * List.length []); (not (x <> []) || not (List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []))) || List.length (interleave_strict x []) <= (List.length x + List.length []); (not (y <> []) || not (List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y); ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)])subproof
((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)start[0.190s, "1.1"] ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)simplify
into ((List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <= ((1 + List.length (List.tl x)) + List.length (List.tl y)) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || not (y <> [])) || not (x <> [])expansions [List.length, List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
simplify
into true
expansions List.length
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
subproof
(not (y <> []) || not (List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y)start[0.190s, "1.2"] (not (y <> []) || not (List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y)simplify
into true
expansions [List.length, List.length, List.length, interleave_strict, List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
subproof
(not (x <> []) || not (List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []))) || List.length (interleave_strict x []) <= (List.length x + List.length [])start[0.190s, "1.3"] (not (x <> []) || not (List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []))) || List.length (interleave_strict x []) <= (List.length x + List.length [])simplify
into true
expansions [List.length, List.length, List.length, interleave_strict, List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
subproof
List.length (interleave_strict [] []) <= (2 * List.length [])start[0.190s, "1.4"] List.length (interleave_strict [] []) <= (2 * List.length [])
simplify
into true
expansions [List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
List.len_nonnegative
len_non_neg
len_nonnegative
rev_len_fc
Loading..
Imandra was able to prove the property using both flavors of structural
induction, but we can see that the proof using the additive flavor was shorter.
Multiplicative schemes will often result in longer proofs than additive schemes,
and thus Imandra uses the additive flavor by default when
[@@induct structural ...] is used.